AArch64 W+R+WW+pospteafp-[dsb.ish]-[isb]+PteAFPte "RfePteAFPte FrePtePteAF PosWWPteAFP DSB.ISH ISB CoePPteAF" variant=precise Cycle=ISB CoePPteAF RfePteAFPte FrePtePteAF PosWWPteAFP DSB.ISH Relax=Pte PteAF Safe=Rfe Fre Coe [PosWW,DSB.ISH,ISB] Generator=diy7 (version 7.56+02~dev) Com=Rf Fr Co Orig=RfePteAFPte FrePtePteAF PosWWPteAFP DSB.ISH ISB CoePPteAF { pteval_t 1:X2; pteval_t 1:X1; pteval_t 0:X2; int x=0; 0:X0=PTE(x); 0:X1=(oa:PA(x), af:0); 1:X0=PTE(x); 2:X0=PTE(x); 2:X1=(oa:PA(x)); 2:X3=x; } P0 | P1 | P2 ; STR X1,[X0] | LDR X1,[X0] | STR X1,[X0] ; LDR X2,[X0] | LDR X2,[X0] | DSB ISH ; | | ISB ; | | MOV W2,#1 ; | | STR W2,[X3] ; exists (0:X2=(oa:PA(x), af:0) /\ 1:X1=(oa:PA(x)) /\ 1:X2=(oa:PA(x), af:0) /\ [x]=0 /\ fault(P2,x,MMU:AccessFlag))